the proof APPEND:

(DECL (*) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 800)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELSE CONS(CAR(U),CDR(U)*V)|)
2. ∀U V.(U*V)=IF NULL(U) THEN V ELSE CONS(CAR(U),CDR(U)*V)
   ctxt: (1 LISP#1 LISP#6 LISP#7 LISP#8)   deps: NIL

(DECSIMP |∀X U V.(CONS(X,U)*V)=CONS(X,U*V)| SRIGHT NIL NIL (LISP#12) 2 LISP#14
 LISP#15 LISP#16)
3. ∀X U V.(CONS(X,U)*V)=CONS(X,U*V)
   ctxt: (1 LISP#1 LISP#2 LISP#6)   deps: NIL

(∀E PHI |λU.LIST(U*V)| LISP#17 LISP#12)
4. LIST(NNIL*V)∧(∀X U.LIST(U*V)⊃LIST(CONS(X,U)*V))⊃(∀U.LIST(U*V))
   ctxt: (1 LISP#1 LISP#2 LISP#5 LISP#6 LISP#9)   deps: NIL

(REWRITE SRIGHT 4 (3 2 LISP#13) LISP#12)
5. (∀X U.LIST(U*V)⊃LIST(CONS(X,U*V)))⊃(∀U.LIST(U*V))
   ctxt: (1 LISP#1 LISP#2 LISP#6 LISP#9)   deps: NIL

(TAUT |∀U V.LIST(U*V)| 5 LISP#12)
6. ∀U V.LIST(U*V)
   ctxt: (1 LISP#1 LISP#9)   deps: NIL

(COMMENTL THE LAST TWO STEPS SHOULD BE DOABLE WITH A SINGLE DECSIMP BUT I HAVE
 NOT BEEN ABLE TO DO IT)